package rdp;
import java.util.Arrays;

import systeme.GrapheRdP;
/**
 * Classe permettant de faire les verifications en avant. On travaille sur les etats successeurs.
 * L'autre classe (CTLArriere fais la meme chose mais ... en arriere c'est a dire sur les etats prédécesseurs)
 */
public class CTL {
	//Prendre le meme code et faire CTL en arriere , dans le grapheRdp on doit ajouter pred
	//il faut que les succ disparaissent
   // int[][] systeme;
   // boolean[][] AP; 
	
	//-->remplacer par rdp
	
	GrapheRdP g_rdp;
	//int etat;

	//--> copier puis ajouter le pred
	//ne plus utiliser le succ mais le pred
	//lire le graphe a lenvers

    public CTL(GrapheRdP g_rdp) {
    	this.g_rdp=g_rdp;
    }

    //est-ce que la place no i est marquée ?
    /**
     * Pour une place donnée, est ce que dans les différents etats du GrapheRdp cette place est marquée ?
     * @param i la place dont on veut savoir si elle est marquée
     * @return un tableau de booleens ex : 110 si c'est la propriete est vraie dans l'etat et l'etat 2
     */
    public boolean[] prop(int i) {
    	
    	boolean[] res=new boolean[g_rdp.etat.size()];
    	Arrays.fill(res,false);
    	//Pour chaque etat
    	for(int j=0; j<g_rdp.etat.size();j++){
    		//Si la place i est marquée dans cet etat
    		if(g_rdp.etat.get(j)[i]){
    			res[j]=true;
    		}
    	}
    	return res;
    }
    
    public boolean[] faux() {
	boolean[] res = new boolean[g_rdp.succ.size()];
	Arrays.fill(res,false);
	return res;
    }

    public boolean[] vrai() {
	boolean[] res = new boolean[g_rdp.succ.size()];
	Arrays.fill(res,true);
	return res;
    }

    public boolean[] neg(boolean[] a) {
	boolean[] res = new boolean[g_rdp.succ.size()];
	for (int i=0; i<g_rdp.succ.size(); i++)
	    res[i] = !a[i];
	return res;
    }
   
    public boolean[] or(boolean[] a, boolean[] b) {
	boolean[] res = new boolean[g_rdp.succ.size()];
	for (int i=0; i<g_rdp.succ.size(); i++)
	    res[i] = a[i] || b[i];
	return res;
    }

    public boolean[] and(boolean[] a, boolean[] b) {
	boolean[] res = new boolean[g_rdp.succ.size()];
	for (int i=0; i<g_rdp.succ.size(); i++)
	    res[i] = a[i] && b[i];
	return res;
    }

    public boolean[] EX(boolean[] a) {
	boolean[] res = new boolean[g_rdp.succ.size()];
	for (int i=0; i<g_rdp.succ.size(); i++) {
	    res[i] = false;
	    for (int j=0; !res[i] && j<g_rdp.succ.get(i).size(); j++)
		res[i] = a[g_rdp.succ.get(i).get(j)];
	}
	return res;
    }

    public boolean[] AX(boolean[] a) {
	return neg(EX(neg(a)));
    } 

    public boolean[] EU(boolean[] a, boolean[] b) {
	boolean[] res = faux();
	boolean[] avant;
    	do {
	    avant = res;
	    res = or(b,and(a,EX(res)));
	} 
	while(!Arrays.equals(avant,res));
	return res;
    }

    public boolean[] AU(boolean[] a, boolean[] b) {
	boolean[] res = faux();
	boolean[] avant;
    	do {
	    avant = res;
	    res = or(b,and(a,AX(res)));
	} 
	while(!Arrays.equals(avant,res));
	return res;
    }
    /*
     * @Djeff
   
    (equivalente)
    public boolean[] prop(int place) {

    	boolean[] res = new boolean[grapheRdp.nbEtat];
    	for (int i = 0 ; i < grapheRdp.nbEtat ; i++){

    	res[i] = grapheRdp.etat.get(i)[place];
    	}

    	return res;

    	}
 
     public boolean[] faux() {
boolean[] res = new boolean[grapheRdp.succ.size()];
Arrays.fill(res,false);
return res;
}
public boolean[] vrai() {
boolean[] res = new boolean[grapheRdp.succ.size()];
Arrays.fill(res,true);
return res;
}
public boolean[] neg(boolean[] a) {
int taille = grapheRdp.succ.size() ;
boolean[] res = new boolean[taille];
for (int i=0; i<taille; i++)
res[i] = !a[i];
return res;
}

public boolean[] or(boolean[] a, boolean[] b) {
int taille = grapheRdp.succ.size();
boolean[] res = new boolean[taille];
for (int i=0; i<taille; i++)
res[i] = a[i] || b[i];
return res;
}
public boolean[] and(boolean[] a, boolean[] b) {

int taille = grapheRdp.succ.size();
boolean[] res = new boolean[taille];
for (int i=0; i<taille; i++)
res[i] = a[i] && b[i];
return res;
}
public boolean[] EX(boolean[] a) {
int taille = grapheRdp.succ.size();
boolean[] res = new boolean[taille];
for (int i=0; i<taille; i++) {
res[i] = false;
for (int j=0; !res[i] && j< grapheRdp.succ.get(i).size(); j++)
res[i] = a[grapheRdp.succ.get(i).get(j)];
}
return res;
}
public boolean[] AX(boolean[] a) {
return neg(EX(neg(a)));
}
     * 
     */
}